Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    merge(nil,y)  → y
2:    merge(x,nil)  → x
3:    merge(x . y,u . v)  → if(x < u,x . merge(y,u . v),u . merge(x . y,v))
4:    nil ++ y  → y
5:    (x . y) ++ z  → x . (y ++ z)
6:    if(true,x,y)  → x
7:    if(false,x,y)  → x
There are 4 dependency pairs:
8:    MERGE(x . y,u . v)  → IF(x < u,x . merge(y,u . v),u . merge(x . y,v))
9:    MERGE(x . y,u . v)  → MERGE(y,u . v)
10:    MERGE(x . y,u . v)  → MERGE(x . y,v)
11:    (x . y) ++# z  → y ++# z
The approximated dependency graph contains 2 SCCs: {11} and {9,10}. Hence the TRS is terminating.
Tyrolean Termination Tool  (0.01 seconds)   ---  May 4, 2006